1. Field of the Invention
The present invention relates to a configurable hardware system implementing Boolean satisfiability (SAT) and method therefor. More specifically, the present invention relates to a field-programmable gate array (FPGA) system operable to obtain a solution set for a SAT problem, and method for using the FPGA system to derive the solution set.
2. Description of the Related Art
The Boolean satisfiability problem lies at the core of many synthesis and verification applications. Therefore, software approaches for accelerating the solution process have been studied extensively. Often, however, particular SAT problems pose computational difficulties for even the most aggressive software approaches. Accordingly, it is desirable to discover new systems and methods for solving complex SAT problems efficiently and rapidly.
Software implementations of SAT have been used to accelerate the solutions of a wide range of problems in synthesis, verification, automatic test pattern generation (ATPG), cryptology, and other fields. Some examples are discussed in S. Chakradhar, V. Agrawal, and S. Rothweiler, A Transitive Closure Algorithm for Test Generation, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 12(7):1015-1028, July 1993; T. Larrabee, Efficient Generation of Test Patterns Using Boolean Satisfiability, PhD thesis, Stanford University, February 1990; and T. Larrabee, Test Pattern Generation Using Boolean Satisfiability, IEEE Transactions on Computer-Aided Design, volume 11, pages 4-15, January 1992. Such software implementations of SAT rely on a backtracking algorithm and other search-space-reducing techniques to explore different possible variable settings, and to determine the implications of these variable settings on the rest of the problem. These methods expand the set of problems for which solutions can be generated in acceptable runtimes. However, for many cases, the prior art software methods are still too slow and at times may have to be aborted before a solution has been obtained.
In order to fully appreciate the present invention, one must have an understanding of SAT and, therefore, it is assumed that the reader is familiar with SAT and with prior art software methods for its implementations. Nevertheless, a short review of SAT and software implementations is provided herein. Additionally, throughout the specification, references are made to various publications describing SAT and prior art software implementations.
Boolean satisfiability (SAT) is a method for finding variable values that satisfy a Boolean formula typically provided in a conjunctive normal form (CNF), i.e., a product of sums. That is, the formula is expressed as an AND of m clauses, each of which is the disjunction (i.e., OR) of one or more literals. Hereinafter, variables (or their complements) taking on an assigned value (1 or 0) are referred to as literals, while a disjunctive expression of literals is referred to as a clause. An x-clause is a clause having x variables. Thus, a set of m clauses defines the SAT in CNF, such as, for example, the set of the two 3-clauses (a+b+d) (a+b+d). Here b is the complement of b.
As discussed in Larrabee cited above, any Boolean satisfiability problems for Boolean formula or circuit can be converted to one for the conjunctive normal form. Those well versed in the art will recognize this as one of several equivalent ways of doing this conversion. Thus, our methods apply to Boolean formulas or circuits in any original form.
According to the prior art methods, the SAT-solver uses a systematic backtracking procedure to obtain a variable assignment for which the CNF formula evaluates to 1. The efficiency of this approach derives from the fact that dependencies between variables can be extracted readily by the nature of the CNF representation. For example, the requirement that the set (b+d) (b+d) evaluate to 1 creates a dependency between the variables b and d, so that d equals to the complement of b. Derivation of such local dependencies allows rapid derivation of non-local dependencies between variables.
The ability to capture non-local implications efficiently, in turn, allows contradictions in variable assignments during the backtracking procedure to be determined rapidly and early. That is, if during variable assignment it is noted that one dependency implies that a=1 and another dependency implies that a=0, then we have a contradiction, i.e., our variable assignment will not lead to a solution and we need to change the assignment.
A number of efficient algorithms have been proposed for SAT in the recent past. For example T. Larrabee, cited above, emphasized the advantage of SAT-based algorithms for automatic test pattern generation (ATPG). Significant enhancements to the basic SAT algorithm are described in S. Chakradhar et al., cited above, and in J. Silva and K. Sakallah, GRASP-A New Search Algorithm for Satisfiability, IEEE ACM International Conference on CAD-96, pages 220-227, November 1996 and P. Stephan, R. Brayton, and A. Sangiovanni-Vincentelli, Combinational Test Generation Using Satisfiability, IEEE Transactions on CAD, Vol. 15, No. 9, Pg 1167-1176, September 1996. In particular, Chakradhar et al. proposed techniques for efficiently deriving and using non-local implications, equivalences and contrapositives. On the other hand, Silva et al. proposed one key advance: a technique for realizing nonlinear backtracking in the SAT solver.
The means of expressing a problem in a conjunctive normal form differ depending on the problem domain. Once the problem has been mapped into the CNF formula, the SAT solver searches for a satisfying assignment for the variables of the CNF. Overall, the solution approach is to assign values to variables one by one, and determine whether their implications on the rest of the clauses in the formula leads to a contradiction. When variables have been assigned to all the variables and the CNF evaluates to one, the SAT has been solved.
However, if an assignment of a particular variable leads to a contradiction, the assignment needs to be changed, or the algorithm needs to backtrack and change a previous assignment(s). More specifically, if a contradiction occurs before the procedure is begun, it indicates that the CNF is unsolvable. If a contradiction occurs after some partial assignments, it indicates that the search can be stopped at that point for these partial assignments. That is, we know that some of the values assigned to variables are leading to a nonsensical solution.
Each step of the backtracking procedure involves two sub-parts. First, a variable to branch on is chosen and is assigned a value. Then the CNF formula is repeatedly updated based on the implications of this variable value until a stopping point is reached, i.e., all the implications have been satisfied or a contradiction occurred. If the second step leads to a contradiction, the search can be stopped at this point and the algorithm can backtrack.
In choosing a value for a variable, there are three possibilities: (a) it may have no value assigned to it at the point the choice is made, (b) the algorithm may be backtracking on the first assignment to the variable, or (c) the algorithm may be backtracking on the second assignment to the variable. In case (a) the algorithm can choose to assign either value (1 or 0) to the variable. In case (b), the algorithm must assign a value that is the opposite of the previous assignment. In case (c) the algorithm must backtrack to the previous variable in the search tree. The algorithm completes when either all the clauses are satisfied or when the search space is exhausted.
Various heuristics can be used to pick the next variable and value to branch on. A common strategy is to pick the literal that occurs in the largest number of clauses.
Consider the example in FIG. 1 for which we need to determine a vector of satisfying assignments. One method of finding such a vector is described below.
Starting from the given clauses of the CNF formula, a data structure is first built, indicating dependencies between literals arising from the 2-clauses. This is illustrated in FIG. 2(a). This data structure will be used to check for implications and contradictions.
Also before beginning the branch-and-bound procedure, values corresponding to the 1-clauses are imposed. We impose the value c=1 in the 1-clause shown in FIG. 1. As a result, some clauses may get satisfied and can be removed from the formula, and some clauses may get smaller, possibly creating new 1 and 2-clauses in the process. The creation of new 2-clauses leads to new dependencies, and the creation of new 1-clauses leads to new values that can be imposed. The process is repeated until no more changes to the CNF formula are possible.
For the example of FIG. 1, we use the initial condition to derive: EQU c=0, g.sub.8 =0.fwdarw.h.sub.h =1.fwdarw.f=0.fwdarw.e=0
Consequently, the remaining clauses are: EQU (a+b) (b+d) (b+d) (a+d)
With the resulting new dependencies: EQU (a+b) (a+d)
When all the 1-clauses have been removed by assigning values to the variables, the remaining clauses can be inspected to determine the literal occurring in the largest number of clauses. A value is imposed on the selected variable and the various derived relationships are used to determine the values of all the variables related to the selected variable.
The execution of this procedure is shown in FIG. 2(b). In this example, the solver first attempts to set the variable a to 1, but it immediately runs into a contradiction by tracing the dependencies transitively on the dependency graph. As a result, it tries the value 0 for the variable a, and finds the satisfying assignment: a=0, b=1.
In more detail, assume the solver first selects the variable a and imposes on it the value 1. Then, from the dependencies, i.e., (a+b), it notes that a=1 implies that b=0, and from (b+d) it notes that b=0 implies d=1. However, from (a+d) it also notes that a=1 implies d=0, which contradicts d=1 from above. Therefore, it must backtrack and change the assignment of a from 1 to 0. This implies that b=1 (from (a+b)). Assigning the value 1 to the variable b, it solves (b+d) (b+d) to find that d=0, which agrees with (a+d). Thus, the assignments a=0 and b=1 satisfies the CNF, i.e., the vector (0,1) is a proper solution to the SAT problem of this example.
Another field of technology which is related to the invention is that of field-programmable gate arrays (FPGA). FPGAs have been an important sector of the integrated circuit market for some time. Traditionally, they have primarily been used for hardware prototyping and design emulation. More specifically, chip designers have been using various FPGA based systems to test their designs and determine their correctness. Such systems include, for example, emulation boards marketed by Aptix, Zycad and Quickform, and reconfigurable computing cards marketed by DEC, Annapolis Microsystems, Altera, Virtual Computing Corp. and Xilinx.
In recent years, however, increasing research interest has focused on using programmable hardware technology for customized computing, rather than just verification of designs. Notable works include P. Athanas and L. Abbott, Real-Time Image Processing on a Custom Computing Platform, IEEE Computer, 28(2):16-24, February 1995; P. M. Athanas and H. F. Silverman, Processor Reconfiguration Through Instruction-Set Metamorphosis, IEEE Computer, March 1993; P. Bertin, D. Roncin, and J. Vuillemin, Introduction to Programmable Active Memories, Technical Report 3, DEC Paris Research Lab, June 1989; P. Dunn, A Configurable Logic Processor for Machine Vision, Field Programmable Logic and Applications, FPL '95, pages 68-77, August 1995; M. Gokhale, W. Holmes, A. Kopser, et al., Building and Using a Highly Parallel Programmable Logic Array, IEEE Computer, 24(1):81-89, January 1991; C. Iseli and E. Sanchez, Spyder: A SURE (Superscalar and Reconfigurable) Processor, Journal of Supercomputing, 9(3):231-252, March 1995; C. Jones, J. Oswald, B. Schoner, and J. Villasenor, Issues in Wireless Video Coding using Run-time-reconfigurable FPGAs, FCCM '95, April 1995; R. Razdan, K. Brace, and M. D. Smith, PRISC software acceleration techniques, Proc. Int'l Conf. on Computer Design, pages 145-149, October 1994; N. Shirazi, A. Walters, and P. Athanas, Quantitative Analysis of Floating Point Arithmetic on FPGA Based Custom Computing Machines, FCCM '95, April 1995. Such work involves identifying computationally-intensive portions of certain applications, and accelerating these portions by implementing them on a computing platform whose characteristics have been specialized for their particular computational requirements.
Using a high level hardware description language (HDL) users can design logic circuits automatically for implementation on FPGAs. Thus, in order to solve a specific problem fast and efficiently, users may opt to design a "problem-specific" specialized logic circuit to solve that particular problem, rather than use a general purpose computer. The problem specific logic circuit would emulate the problem to be solved, and would provide solutions depending on the input data provided.
In general, there are several application characteristics that make a problem amenable to a configurable hardware implementation. These include (i) limited bit-width computations, (ii) computations with frequent logical operations, and (iii) problems with more instruction-level parallelism than available in current microprocessors. These characteristics make the applications easy to map to configurable hardware, and accentuate the differences between a general-purpose processor and a configurable implementation. Boolean satisfiability is thus a promising application because it requires performing a large number of potentially-parallel logical operations.
Although configurable hardware designs are quite flexible and diverse, there are several FPGA characteristics that help shape the designs overall. First, FPGAs are made up of many repeated design elements often referred to as Configurable Logic Blocks (CLBs). The size and makeup of the CLB depends on the maker and product line of the FPGA, but they typically contain a small number of flip-flops and are able to form logic functions of roughly 3-9 inputs.
The CLBs in an FPGA are interconnected via a routing network. Most FPGAs have mechanisms for both near-neighbor as well as non-local communication between CLBS. Since non-local communication may increase computation time, most configurable applications attempt to exploit local routing connections by requiring mainly near-neighbor communication between blocks of the circuit. Some FPGA architectures also have mechanisms for using longer routing wires to form wired-logic between many CLB outputs. These mechanisms are particularly useful when an application requires large-input OR or AND gates.
One method for using FPGA to implement SAT is disclosed by T. Suyama, M. Yokoo, and H. Sawada, Solving Satisfiability Problems on FPGAS. 6th Int'l Workshop on Field-Programmable Logic and Applications, September 1996. Suyama et al. teach to create on an FPGA a logic circuit corresponding to the SAT problem to be solved, and to apply a vector (consisting of value assignments to all the variables simultaneously) to check all the constraints concurrently. More specifically, Suyama defines a vector consisting of n-digit binary value to represent the assignments of all the variables concurrently, so that the value assignment of the a.sub.i variable is represented by the i.sup.th digit of the binary value. This vector is applied to the FPGA and the output of the FPGA is checked to determine whether the vector is a solution. Accordingly, the system of Suyama does not develop the dependencies between the variables and does not perform a branch and bound process.
As can be appreciated, in its exhaustive form, the algorithm of Suyama et al. sequentially increments the n-digit binary value and simultaneously checks whether all the clauses are satisfied. If all the clauses are satisfied, the binary value is recorded as a solution. In its more efficient form, the algorithm of Suyama et al. increments the variable with the lowest index included in the unsatisfied clauses so as to reduce the search space. Thus, Suyama basically maps the problem onto the FPGA and tries various values to check whether they correspond to a solution. This is similar to one trying to unlock a combinational lock by exhaustively trying different numbers until the lock opens.
However, the algorithm of Suyama visits a very large number of states before arriving at a solution (reportedly three to eight times the number of states visited by the comparative Davis-Putnam procedure M. Davis, H. Putnam, "A Computing Procedure for Quantification Theory" Journal of the ACA, Vol. 7, Pages 201-215, 1960). Additionally, it is unclear if and how various heuristics and dynamic ordering schemes used to prune the search space can be implemented in the algorithm of Suyama et al. so as to increase its efficiency so as to provide rapid solutions to complex problems. Importantly, the complexity of implementing the method of Suyama rapidly increases with the complexity of the problem to be solved.